((v6 v9 9) (v8 v10 0) (v8 v1 2) (v11 v12 7) (v11 v9 1) (v6 v2 9) (v9 v10 4) (v6 v1 7) (v3 v8 9) (v6 v10 7) (v7 v8 2) (v4 v6 0) (v12 v9 1) (v4 v10 0) (v9 v4 1) (v10 v12 5) (v12 v3 3) (v7 v2 6) (v6 v11 6) (v6 v8 4) (v12 v1 3) (v5 v1 6) (v4 v11 8) (v10 v1 1) (v2 v3 1) (v2 v12 2) (v3 v4 0) (v2 v4 5) (v6 v5 0) (v1 v4 9) (v11 v2 2) (v5 v9 1) (v9 v2 9) (v6 v7 3) (v10 v3 5) (v8 v2 3) (v1 v3 6) (v4 v8 7))
158
((v8 v11) (v3 v4) (v10 v2))